Nuprl Definition : sem-satisfiable
11,40
postcript
pdf
X
==
pr
:
Pgm
.
pr
|=
X
latex
clarification:
sem-satisfiable(
S
;
Pgm
;
X
) ==
pr
:
Pgm
. sem-sat(
S
;
pr
;
X
)
latex
Definitions
x
:
A
.
B
(
x
)
,
pr
|=
X
FDL editor aliases
sem-satisfiable
origin
X == 
pr:Pgm. pr |= X
pr:Pgm. sem-sat(S;pr;X) X == pr:Pgm. pr |= X
pr:Pgm. sem-sat(S;pr;X) x:A. B(x)